My mathematical logic is rusty, but if I’m not mistaken, the relevant criterion is that the set of axioms must be recursively enumerable, i.e. either finite or with a countable number of axioms that are generated using some Turing-equivalent sort of axiom schemas.
A countable set of axioms can be non-recursively-enumerable (i.e. there’s no Turing machine that generates its members, and nothing else, as output). Such sets of axioms clearly cannot be Goedelized, since there are uncountably many of them—whereas for recursively enumerable ones, it’s only necessary to enumerate the Turing machines that generate them.
I think recursively enumerable is sufficient but not necessary. To see an example, consider Peano Arithmetic with added axioms as follows: Pick some lexographic ordering of all well-formed formula in PA, and denote this system by P_0. Define Pn for n>1 by running through your list of statements until you come to one that isn’t provable or disprovable in P(n-1). When you do, throw it in as true with the axioms of P_(n-1) to get P_n. Consider then the system P_infinity = the union of all the P_i. This system has only finitely many axioms, is Godel numerable by most definitions of that term but is not recursively enumerable (since if it were we’d have a decision procedure for PA.)
Yes, you’re right, of course. In my above comment, I failed to consider that not only Turing machines can be Goedelized, but also various infinite-step procedures that produce non-computable results, such as the one you outlined above.
(Also, I assume you meant “countably,” not “finitely” in the last sentence.)
My mathematical logic is rusty, but if I’m not mistaken, the relevant criterion is that the set of axioms must be recursively enumerable, i.e. either finite or with a countable number of axioms that are generated using some Turing-equivalent sort of axiom schemas.
A countable set of axioms can be non-recursively-enumerable (i.e. there’s no Turing machine that generates its members, and nothing else, as output). Such sets of axioms clearly cannot be Goedelized, since there are uncountably many of them—whereas for recursively enumerable ones, it’s only necessary to enumerate the Turing machines that generate them.
I think recursively enumerable is sufficient but not necessary. To see an example, consider Peano Arithmetic with added axioms as follows: Pick some lexographic ordering of all well-formed formula in PA, and denote this system by P_0. Define Pn for n>1 by running through your list of statements until you come to one that isn’t provable or disprovable in P(n-1). When you do, throw it in as true with the axioms of P_(n-1) to get P_n. Consider then the system P_infinity = the union of all the P_i. This system has only finitely many axioms, is Godel numerable by most definitions of that term but is not recursively enumerable (since if it were we’d have a decision procedure for PA.)
Yes, you’re right, of course. In my above comment, I failed to consider that not only Turing machines can be Goedelized, but also various infinite-step procedures that produce non-computable results, such as the one you outlined above.
(Also, I assume you meant “countably,” not “finitely” in the last sentence.)